Nuprl Definition : ma-interface-domb
11,40
postcript
pdf
ma-interface-domb(
I
;
i
;
k
) ==
k
dom(
I
(
i
).2)
latex
clarification:
ma-interface-domb(
I
;
i
;
k
) == fpf-dom(KindDeq;
k
; (
I
IdDeq(
i
).2))
latex
Definitions
x
dom(
f
)
,
KindDeq
,
t
.2
,
f
(
x
)
,
IdDeq
FDL editor aliases
ma-interface-domb
origin
dom(I(i).2)
dom(I(i).2)
dom(f)